A:Type, es:ES, I:AbsInterface(A), P:(E), p:(e:E. Dec(P(e))), e:E.
((e  (I|p)))  {((e  I)) & P(e)} 

latex

Definitions	x:A. B(x), x(s), P & Q, b, f(a), x:A  B(x), P  Q, P  Q, P  Q, Type, , t  T, Top, x:AB(x), S  T, left + right, E, suptype(S; T), can-apply(f;x), Void, x:A.B(x), x.A(x), x. t(x), p-restrict(f;p), ES, Dec(P), {T}, e  X, (I|p), AbsInterface(A)
Lemmas	decidable wf, es-E wf, event system wf, iff functionality wrt iff, can-apply-p-restrict, p-restrict wf, top wf, can-apply wf, assert wf